1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]3. $u$ : $T$
\\[0ex]4. $v$ : $T$ List
\\[0ex]5. $\forall$$n$:\{0$\ldots\,\parallel$$v$$\parallel$\}, $i$:\{0..($\parallel$$v$$\parallel$ {-} $n$)$^{-}$\}. nth\_tl($n$;$v$)[$i$] = $v$[($i$+$n$)]
\\[0ex]$\vdash$  $\forall$$n$:\{0$\ldots\,\parallel$$v$$\parallel$+1\}, $i$:\{0..(($\parallel$$v$$\parallel$+1) {-} $n$)$^{-}$\}. nth\_tl($n$;[$u$ / $v$])[$i$] = [$u$ / $v$][($i$+$n$)]